(1
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 118)
  ("(var3 stable)" 118 182)
  ("(var3 up)" 182 186)
  ("(var3 down)" 186 194)
  ("(var3 stable)" 194 196)
  ("(var3 up)" 196 200)
  ("(var3 stable)" 200 322)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 118)
  ("(var4 stable)" 118 192)
  ("(var4 down)" 192 304)
  ("(var4 stable)" 304 322)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 108)
  ("(var1 stable)" 108 322)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 212)
  ("(var2 stable)" 212 322)
 )
)
(2
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 84)
  ("(var3 stable)" 84 86)
  ("(var3 up)" 86 116)
  ("(var3 stable)" 116 201)
  ("(var3 up)" 201 206)
  ("(var3 down)" 206 215)
  ("(var3 up)" 215 220)
  ("(var3 stable)" 220 360)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 88)
  ("(var4 stable)" 88 90)
  ("(var4 up)" 90 122)
  ("(var4 stable)" 122 222)
  ("(var4 down)" 222 312)
  ("(var4 stable)" 312 360)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 117)
  ("(var1 stable)" 117 360)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 103)
  ("(var2 down)" 103 108)
  ("(var2 up)" 108 248)
  ("(var2 down)" 248 250)
  ("(var2 up)" 250 253)
  ("(var2 stable)" 253 360)
 )
)
(3
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 75)
  ("(var3 down)" 75 77)
  ("(var3 stable)" 77 149)
  ("(var3 up)" 149 153)
  ("(var3 stable)" 153 155)
  ("(var3 down)" 155 164)
  ("(var3 up)" 164 170)
  ("(var3 stable)" 170 302)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 67)
  ("(var4 stable)" 67 157)
  ("(var4 down)" 157 258)
  ("(var4 stable)" 258 302)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 64)
  ("(var1 stable)" 64 302)
  ("(var2 stable)" 0 56)
  ("(var2 up)" 56 58)
  ("(var2 down)" 58 62)
  ("(var2 up)" 62 191)
  ("(var2 down)" 191 193)
  ("(var2 stable)" 193 302)
 )
)
(4
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 73)
  ("(var3 down)" 73 76)
  ("(var3 up)" 76 80)
  ("(var3 stable)" 80 154)
  ("(var3 down)" 154 156)
  ("(var3 up)" 156 162)
  ("(var3 down)" 162 173)
  ("(var3 up)" 173 179)
  ("(var3 stable)" 179 312)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 79)
  ("(var4 stable)" 79 176)
  ("(var4 down)" 176 267)
  ("(var4 up)" 267 269)
  ("(var4 down)" 269 271)
  ("(var4 up)" 271 273)
  ("(var4 down)" 273 275)
  ("(var4 stable)" 275 312)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 71)
  ("(var1 down)" 71 73)
  ("(var1 stable)" 73 312)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 66)
  ("(var2 stable)" 66 109)
  ("(var2 up)" 109 199)
  ("(var2 stable)" 199 312)
 )
)
(5
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 95)
  ("(var3 stable)" 95 164)
  ("(var3 up)" 164 170)
  ("(var3 down)" 170 178)
  ("(var3 stable)" 178 180)
  ("(var3 up)" 180 184)
  ("(var3 stable)" 184 310)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 90)
  ("(var4 down)" 90 92)
  ("(var4 up)" 92 97)
  ("(var4 stable)" 97 182)
  ("(var4 down)" 182 184)
  ("(var4 up)" 184 186)
  ("(var4 down)" 186 275)
  ("(var4 stable)" 275 310)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 73)
  ("(var1 down)" 73 75)
  ("(var1 up)" 75 92)
  ("(var1 stable)" 92 310)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 86)
  ("(var2 up)" 86 122)
  ("(var2 stable)" 122 124)
  ("(var2 up)" 124 208)
  ("(var2 stable)" 208 310)
 )
)
(6
 (
  ("(var3 stable)" 0 93)
  ("(var3 up)" 93 117)
  ("(var3 stable)" 117 122)
  ("(var3 up)" 122 124)
  ("(var3 stable)" 124 205)
  ("(var3 up)" 205 210)
  ("(var3 down)" 210 221)
  ("(var3 up)" 221 227)
  ("(var3 stable)" 227 368)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 88)
  ("(var4 stable)" 88 92)
  ("(var4 up)" 92 121)
  ("(var4 stable)" 121 131)
  ("(var4 down)" 131 133)
  ("(var4 stable)" 133 227)
  ("(var4 down)" 227 257)
  ("(var4 stable)" 257 259)
  ("(var4 down)" 259 353)
  ("(var4 stable)" 353 368)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 123)
  ("(var1 stable)" 123 368)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 up)" 110 197)
  ("(var2 stable)" 197 199)
  ("(var2 up)" 199 234)
  ("(var2 stable)" 234 368)
 )
)
(7
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 44)
  ("(var3 stable)" 44 46)
  ("(var3 up)" 46 72)
  ("(var3 stable)" 72 150)
  ("(var3 up)" 150 156)
  ("(var3 down)" 156 165)
  ("(var3 up)" 165 170)
  ("(var3 stable)" 170 172)
  ("(var3 up)" 172 174)
  ("(var3 stable)" 174 302)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 74)
  ("(var4 stable)" 74 163)
  ("(var4 down)" 163 269)
  ("(var4 stable)" 269 302)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 68)
  ("(var1 down)" 68 70)
  ("(var1 up)" 70 74)
  ("(var1 stable)" 74 302)
  ("(var2 stable)" 0 56)
  ("(var2 up)" 56 58)
  ("(var2 down)" 58 63)
  ("(var2 up)" 63 186)
  ("(var2 stable)" 186 302)
 )
)
(8
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 75)
  ("(var3 down)" 75 77)
  ("(var3 up)" 77 99)
  ("(var3 stable)" 99 188)
  ("(var3 up)" 188 190)
  ("(var3 stable)" 190 192)
  ("(var3 down)" 192 200)
  ("(var3 up)" 200 206)
  ("(var3 stable)" 206 346)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 66)
  ("(var4 down)" 66 68)
  ("(var4 up)" 68 101)
  ("(var4 stable)" 101 228)
  ("(var4 down)" 228 299)
  ("(var4 stable)" 299 346)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 96)
  ("(var1 down)" 96 98)
  ("(var1 stable)" 98 346)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 88)
  ("(var2 down)" 88 92)
  ("(var2 up)" 92 219)
  ("(var2 stable)" 219 346)
 )
)
(9
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 96)
  ("(var3 stable)" 96 173)
  ("(var3 up)" 173 179)
  ("(var3 down)" 179 189)
  ("(var3 up)" 189 194)
  ("(var3 stable)" 194 328)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 96)
  ("(var4 stable)" 96 183)
  ("(var4 up)" 183 186)
  ("(var4 down)" 186 280)
  ("(var4 up)" 280 283)
  ("(var4 stable)" 283 328)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 67)
  ("(var1 down)" 67 69)
  ("(var1 up)" 69 90)
  ("(var1 stable)" 90 328)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 199)
  ("(var2 down)" 199 201)
  ("(var2 up)" 201 203)
  ("(var2 stable)" 203 328)
 )
)
(10
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 115)
  ("(var3 stable)" 115 196)
  ("(var3 up)" 196 200)
  ("(var3 stable)" 200 202)
  ("(var3 down)" 202 211)
  ("(var3 up)" 211 216)
  ("(var3 stable)" 216 352)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 118)
  ("(var4 stable)" 118 236)
  ("(var4 down)" 236 312)
  ("(var4 stable)" 312 352)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 109)
  ("(var1 stable)" 109 352)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 stable)" 105 147)
  ("(var2 up)" 147 231)
  ("(var2 down)" 231 233)
  ("(var2 stable)" 233 352)
 )
)
(11
 (
  ("(var3 stable)" 0 86)
  ("(var3 up)" 86 107)
  ("(var3 stable)" 107 109)
  ("(var3 up)" 109 112)
  ("(var3 stable)" 112 185)
  ("(var3 up)" 185 191)
  ("(var3 down)" 191 201)
  ("(var3 up)" 201 207)
  ("(var3 stable)" 207 334)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 120)
  ("(var4 stable)" 120 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 294)
  ("(var4 stable)" 294 334)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 108)
  ("(var1 stable)" 108 334)
  ("(var2 stable)" 0 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 104)
  ("(var2 stable)" 104 135)
  ("(var2 up)" 135 225)
  ("(var2 stable)" 225 334)
 )
)
(12
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 115)
  ("(var3 stable)" 115 117)
  ("(var3 up)" 117 130)
  ("(var3 stable)" 130 212)
  ("(var3 up)" 212 218)
  ("(var3 down)" 218 229)
  ("(var3 up)" 229 232)
  ("(var3 stable)" 232 371)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 138)
  ("(var4 stable)" 138 259)
  ("(var4 down)" 259 310)
  ("(var4 up)" 310 312)
  ("(var4 down)" 312 335)
  ("(var4 stable)" 335 371)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 120)
  ("(var1 down)" 120 122)
  ("(var1 up)" 122 127)
  ("(var1 stable)" 127 371)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 111)
  ("(var2 down)" 111 114)
  ("(var2 up)" 114 275)
  ("(var2 stable)" 275 371)
 )
)
(13
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 84)
  ("(var3 stable)" 84 158)
  ("(var3 up)" 158 162)
  ("(var3 down)" 162 173)
  ("(var3 up)" 173 177)
  ("(var3 stable)" 177 311)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 52)
  ("(var4 stable)" 52 54)
  ("(var4 up)" 54 78)
  ("(var4 stable)" 78 173)
  ("(var4 down)" 173 269)
  ("(var4 stable)" 269 311)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 78)
  ("(var1 down)" 78 80)
  ("(var1 stable)" 80 311)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 up)" 70 176)
  ("(var2 stable)" 176 311)
 )
)
(14
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 79)
  ("(var3 stable)" 79 157)
  ("(var3 up)" 157 163)
  ("(var3 down)" 163 173)
  ("(var3 up)" 173 176)
  ("(var3 stable)" 176 303)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 85)
  ("(var4 down)" 85 87)
  ("(var4 stable)" 87 184)
  ("(var4 down)" 184 264)
  ("(var4 stable)" 264 303)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 78)
  ("(var1 stable)" 78 303)
  ("(var2 stable)" 0 65)
  ("(var2 up)" 65 67)
  ("(var2 down)" 67 72)
  ("(var2 up)" 72 179)
  ("(var2 stable)" 179 301)
  ("(var2 down)" 301 303)
 )
)
(15
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 107)
  ("(var3 stable)" 107 178)
  ("(var3 up)" 178 184)
  ("(var3 down)" 184 192)
  ("(var3 up)" 192 198)
  ("(var3 stable)" 198 315)
  ("(var3 down)" 315 317)
  ("(var4 up)" 0 2)
  ("(var4 down)" 2 4)
  ("(var4 stable)" 4 77)
  ("(var4 up)" 77 79)
  ("(var4 stable)" 79 81)
  ("(var4 up)" 81 103)
  ("(var4 stable)" 103 217)
  ("(var4 down)" 217 282)
  ("(var4 stable)" 282 317)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 104)
  ("(var1 stable)" 104 317)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 94)
  ("(var2 down)" 94 98)
  ("(var2 up)" 98 220)
  ("(var2 stable)" 220 317)
 )
)
(16
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 91)
  ("(var3 stable)" 91 174)
  ("(var3 up)" 174 178)
  ("(var3 down)" 178 186)
  ("(var3 up)" 186 191)
  ("(var3 stable)" 191 326)
  ("(var4 stable)" 0 60)
  ("(var4 down)" 60 62)
  ("(var4 up)" 62 98)
  ("(var4 stable)" 98 211)
  ("(var4 down)" 211 275)
  ("(var4 up)" 275 277)
  ("(var4 down)" 277 288)
  ("(var4 stable)" 288 326)
  ("(var1 up)" 0 4)
  ("(var1 stable)" 4 65)
  ("(var1 up)" 65 87)
  ("(var1 stable)" 87 326)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 220)
  ("(var2 stable)" 220 326)
 )
)
(17
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 93)
  ("(var3 stable)" 93 172)
  ("(var3 up)" 172 176)
  ("(var3 down)" 176 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 315)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 96)
  ("(var4 stable)" 96 176)
  ("(var4 down)" 176 312)
  ("(var4 up)" 312 315)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 89)
  ("(var1 stable)" 89 315)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 85)
  ("(var2 up)" 85 251)
  ("(var2 stable)" 251 315)
 )
)
(18
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 72)
  ("(var3 stable)" 72 147)
  ("(var3 up)" 147 152)
  ("(var3 down)" 152 163)
  ("(var3 up)" 163 165)
  ("(var3 stable)" 165 295)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 74)
  ("(var4 stable)" 74 178)
  ("(var4 down)" 178 249)
  ("(var4 up)" 249 251)
  ("(var4 down)" 251 255)
  ("(var4 up)" 255 257)
  ("(var4 down)" 257 259)
  ("(var4 stable)" 259 295)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 67)
  ("(var1 stable)" 67 295)
  ("(var2 stable)" 0 58)
  ("(var2 up)" 58 60)
  ("(var2 down)" 60 64)
  ("(var2 stable)" 64 98)
  ("(var2 up)" 98 186)
  ("(var2 stable)" 186 295)
 )
)
(19
 (
  ("(var3 stable)" 0 52)
  ("(var3 down)" 52 55)
  ("(var3 up)" 55 85)
  ("(var3 stable)" 85 163)
  ("(var3 up)" 163 168)
  ("(var3 down)" 168 179)
  ("(var3 up)" 179 183)
  ("(var3 stable)" 183 317)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 88)
  ("(var4 stable)" 88 182)
  ("(var4 down)" 182 214)
  ("(var4 up)" 214 216)
  ("(var4 down)" 216 261)
  ("(var4 stable)" 261 264)
  ("(var4 down)" 264 268)
  ("(var4 up)" 268 270)
  ("(var4 down)" 270 272)
  ("(var4 stable)" 272 317)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 85)
  ("(var1 stable)" 85 317)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 73)
  ("(var2 down)" 73 77)
  ("(var2 stable)" 77 120)
  ("(var2 up)" 120 216)
  ("(var2 stable)" 216 317)
 )
)
(20
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 95)
  ("(var3 down)" 95 97)
  ("(var3 stable)" 97 166)
  ("(var3 up)" 166 170)
  ("(var3 down)" 170 180)
  ("(var3 up)" 180 183)
  ("(var3 stable)" 183 311)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 95)
  ("(var4 stable)" 95 171)
  ("(var4 down)" 171 265)
  ("(var4 up)" 265 267)
  ("(var4 stable)" 267 308)
  ("(var4 up)" 308 311)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 65)
  ("(var1 down)" 65 67)
  ("(var1 up)" 67 88)
  ("(var1 stable)" 88 311)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 181)
  ("(var2 stable)" 181 183)
  ("(var2 up)" 183 185)
  ("(var2 stable)" 185 311)
 )
)
(21
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 134)
  ("(var3 stable)" 134 214)
  ("(var3 up)" 214 218)
  ("(var3 down)" 218 227)
  ("(var3 stable)" 227 376)
  ("(var4 stable)" 0 95)
  ("(var4 up)" 95 120)
  ("(var4 stable)" 120 122)
  ("(var4 up)" 122 128)
  ("(var4 stable)" 128 232)
  ("(var4 down)" 232 327)
  ("(var4 up)" 327 329)
  ("(var4 down)" 329 331)
  ("(var4 stable)" 331 376)
  ("(var1 stable)" 0 99)
  ("(var1 up)" 99 101)
  ("(var1 down)" 101 103)
  ("(var1 up)" 103 130)
  ("(var1 stable)" 130 376)
  ("(var2 stable)" 0 111)
  ("(var2 up)" 111 113)
  ("(var2 down)" 113 118)
  ("(var2 up)" 118 246)
  ("(var2 stable)" 246 376)
 )
)
(22
 (
  ("(var3 stable)" 0 40)
  ("(var3 down)" 40 42)
  ("(var3 up)" 42 71)
  ("(var3 stable)" 71 154)
  ("(var3 up)" 154 159)
  ("(var3 down)" 159 168)
  ("(var3 up)" 168 173)
  ("(var3 stable)" 173 313)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 71)
  ("(var4 stable)" 71 74)
  ("(var4 up)" 74 76)
  ("(var4 stable)" 76 166)
  ("(var4 down)" 166 293)
  ("(var4 stable)" 293 313)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 66)
  ("(var1 stable)" 66 313)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 58)
  ("(var2 down)" 58 62)
  ("(var2 up)" 62 173)
  ("(var2 stable)" 173 313)
 )
)
(23
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 96)
  ("(var3 down)" 96 98)
  ("(var3 stable)" 98 175)
  ("(var3 up)" 175 180)
  ("(var3 down)" 180 190)
  ("(var3 up)" 190 194)
  ("(var3 stable)" 194 323)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 98)
  ("(var4 stable)" 98 193)
  ("(var4 down)" 193 275)
  ("(var4 stable)" 275 278)
  ("(var4 down)" 278 284)
  ("(var4 stable)" 284 323)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 101)
  ("(var1 stable)" 101 323)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 84)
  ("(var2 down)" 84 89)
  ("(var2 up)" 89 215)
  ("(var2 stable)" 215 321)
  ("(var2 down)" 321 323)
 )
)
(24
 (
  ("(var3 stable)" 0 12)
  ("(var3 up)" 12 58)
  ("(var3 stable)" 58 139)
  ("(var3 up)" 139 142)
  ("(var3 stable)" 142 144)
  ("(var3 down)" 144 153)
  ("(var3 up)" 153 158)
  ("(var3 stable)" 158 283)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 64)
  ("(var4 stable)" 64 167)
  ("(var4 down)" 167 171)
  ("(var4 stable)" 171 174)
  ("(var4 down)" 174 239)
  ("(var4 stable)" 239 283)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 30)
  ("(var1 down)" 30 32)
  ("(var1 up)" 32 62)
  ("(var1 stable)" 62 283)
  ("(var2 stable)" 0 45)
  ("(var2 up)" 45 47)
  ("(var2 down)" 47 52)
  ("(var2 up)" 52 160)
  ("(var2 stable)" 160 162)
  ("(var2 up)" 162 170)
  ("(var2 stable)" 170 283)
 )
)
(25
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 99)
  ("(var3 stable)" 99 189)
  ("(var3 up)" 189 193)
  ("(var3 stable)" 193 195)
  ("(var3 down)" 195 205)
  ("(var3 up)" 205 212)
  ("(var3 stable)" 212 360)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 106)
  ("(var4 stable)" 106 237)
  ("(var4 down)" 237 312)
  ("(var4 stable)" 312 360)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 73)
  ("(var1 down)" 73 76)
  ("(var1 up)" 76 113)
  ("(var1 stable)" 113 360)
  ("(var2 stable)" 0 87)
  ("(var2 up)" 87 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 235)
  ("(var2 down)" 235 237)
  ("(var2 stable)" 237 360)
 )
)
(26
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 87)
  ("(var3 stable)" 87 167)
  ("(var3 up)" 167 170)
  ("(var3 stable)" 170 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 323)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 81)
  ("(var4 stable)" 81 83)
  ("(var4 up)" 83 85)
  ("(var4 stable)" 85 205)
  ("(var4 down)" 205 280)
  ("(var4 stable)" 280 320)
  ("(var4 up)" 320 323)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 81)
  ("(var1 stable)" 81 323)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 69)
  ("(var2 down)" 69 74)
  ("(var2 stable)" 74 120)
  ("(var2 up)" 120 212)
  ("(var2 stable)" 212 321)
  ("(var2 down)" 321 323)
 )
)
(27
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 120)
  ("(var3 stable)" 120 193)
  ("(var3 up)" 193 199)
  ("(var3 down)" 199 209)
  ("(var3 up)" 209 211)
  ("(var3 stable)" 211 343)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 86)
  ("(var4 down)" 86 88)
  ("(var4 up)" 88 113)
  ("(var4 down)" 113 115)
  ("(var4 stable)" 115 207)
  ("(var4 down)" 207 311)
  ("(var4 stable)" 311 343)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 111)
  ("(var1 stable)" 111 343)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 107)
  ("(var2 up)" 107 229)
  ("(var2 stable)" 229 343)
 )
)
(28
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 66)
  ("(var3 down)" 66 68)
  ("(var3 up)" 68 71)
  ("(var3 stable)" 71 152)
  ("(var3 up)" 152 157)
  ("(var3 down)" 157 167)
  ("(var3 up)" 167 174)
  ("(var3 stable)" 174 315)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 71)
  ("(var4 stable)" 71 167)
  ("(var4 down)" 167 284)
  ("(var4 stable)" 284 315)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 37)
  ("(var1 stable)" 37 41)
  ("(var1 up)" 41 64)
  ("(var1 stable)" 64 315)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 54)
  ("(var2 down)" 54 59)
  ("(var2 stable)" 59 104)
  ("(var2 up)" 104 157)
  ("(var2 stable)" 157 161)
  ("(var2 up)" 161 194)
  ("(var2 stable)" 194 315)
 )
)
(29
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 125)
  ("(var3 stable)" 125 206)
  ("(var3 up)" 206 214)
  ("(var3 down)" 214 225)
  ("(var3 stable)" 225 372)
  ("(var4 stable)" 0 92)
  ("(var4 up)" 92 94)
  ("(var4 down)" 94 97)
  ("(var4 up)" 97 123)
  ("(var4 stable)" 123 125)
  ("(var4 up)" 125 127)
  ("(var4 stable)" 127 255)
  ("(var4 down)" 255 257)
  ("(var4 up)" 257 259)
  ("(var4 down)" 259 349)
  ("(var4 stable)" 349 372)
  ("(var1 stable)" 0 99)
  ("(var1 up)" 99 101)
  ("(var1 down)" 101 103)
  ("(var1 up)" 103 125)
  ("(var1 stable)" 125 372)
  ("(var2 stable)" 0 110)
  ("(var2 up)" 110 112)
  ("(var2 down)" 112 117)
  ("(var2 up)" 117 252)
  ("(var2 stable)" 252 372)
 )
)
(30
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 53)
  ("(var3 down)" 53 56)
  ("(var3 up)" 56 79)
  ("(var3 stable)" 79 81)
  ("(var3 up)" 81 89)
  ("(var3 stable)" 89 169)
  ("(var3 up)" 169 173)
  ("(var3 down)" 173 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 321)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 91)
  ("(var4 down)" 91 93)
  ("(var4 up)" 93 95)
  ("(var4 stable)" 95 188)
  ("(var4 down)" 188 281)
  ("(var4 stable)" 281 321)
  ("(var1 stable)" 0 54)
  ("(var1 up)" 54 81)
  ("(var1 stable)" 81 321)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 up)" 76 200)
  ("(var2 stable)" 200 321)
 )
)
(31
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 61)
  ("(var3 stable)" 61 66)
  ("(var3 up)" 66 101)
  ("(var3 stable)" 101 179)
  ("(var3 up)" 179 187)
  ("(var3 down)" 187 196)
  ("(var3 up)" 196 199)
  ("(var3 stable)" 199 341)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 102)
  ("(var4 stable)" 102 204)
  ("(var4 down)" 204 297)
  ("(var4 stable)" 297 341)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 76)
  ("(var1 stable)" 76 78)
  ("(var1 up)" 78 100)
  ("(var1 stable)" 100 341)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 stable)" 92 131)
  ("(var2 up)" 131 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 223)
  ("(var2 down)" 223 225)
  ("(var2 up)" 225 227)
  ("(var2 down)" 227 230)
  ("(var2 up)" 230 232)
  ("(var2 stable)" 232 341)
 )
)
(32
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 119)
  ("(var3 stable)" 119 203)
  ("(var3 up)" 203 206)
  ("(var3 stable)" 206 208)
  ("(var3 down)" 208 216)
  ("(var3 stable)" 216 218)
  ("(var3 up)" 218 221)
  ("(var3 stable)" 221 360)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 87)
  ("(var4 down)" 87 89)
  ("(var4 up)" 89 116)
  ("(var4 stable)" 116 120)
  ("(var4 up)" 120 122)
  ("(var4 stable)" 122 248)
  ("(var4 down)" 248 333)
  ("(var4 stable)" 333 360)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 122)
  ("(var1 stable)" 122 358)
  ("(var1 down)" 358 360)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 105)
  ("(var2 down)" 105 110)
  ("(var2 up)" 110 211)
  ("(var2 stable)" 211 213)
  ("(var2 up)" 213 215)
  ("(var2 stable)" 215 360)
 )
)
(33
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 123)
  ("(var3 stable)" 123 193)
  ("(var3 up)" 193 199)
  ("(var3 down)" 199 207)
  ("(var3 up)" 207 211)
  ("(var3 stable)" 211 336)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 121)
  ("(var4 stable)" 121 217)
  ("(var4 down)" 217 307)
  ("(var4 stable)" 307 336)
  ("(var1 stable)" 0 90)
  ("(var1 up)" 90 116)
  ("(var1 stable)" 116 336)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 up)" 109 156)
  ("(var2 stable)" 156 159)
  ("(var2 up)" 159 235)
  ("(var2 stable)" 235 336)
 )
)
(34
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 106)
  ("(var3 stable)" 106 177)
  ("(var3 up)" 177 182)
  ("(var3 down)" 182 188)
  ("(var3 up)" 188 192)
  ("(var3 stable)" 192 320)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 79)
  ("(var4 stable)" 79 81)
  ("(var4 up)" 81 106)
  ("(var4 stable)" 106 192)
  ("(var4 down)" 192 290)
  ("(var4 stable)" 290 320)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 100)
  ("(var1 stable)" 100 320)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 206)
  ("(var2 stable)" 206 320)
 )
)
(35
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 65)
  ("(var3 down)" 65 67)
  ("(var3 up)" 67 94)
  ("(var3 stable)" 94 171)
  ("(var3 up)" 171 174)
  ("(var3 stable)" 174 176)
  ("(var3 down)" 176 184)
  ("(var3 up)" 184 192)
  ("(var3 stable)" 192 328)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 88)
  ("(var4 stable)" 88 214)
  ("(var4 down)" 214 279)
  ("(var4 stable)" 279 284)
  ("(var4 down)" 284 286)
  ("(var4 stable)" 286 328)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 94)
  ("(var1 stable)" 94 328)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 stable)" 79 123)
  ("(var2 up)" 123 210)
  ("(var2 down)" 210 212)
  ("(var2 up)" 212 216)
  ("(var2 stable)" 216 328)
 )
)
(36
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 109)
  ("(var3 stable)" 109 111)
  ("(var3 up)" 111 129)
  ("(var3 stable)" 129 132)
  ("(var3 up)" 132 134)
  ("(var3 stable)" 134 219)
  ("(var3 up)" 219 223)
  ("(var3 down)" 223 235)
  ("(var3 up)" 235 239)
  ("(var3 stable)" 239 386)
  ("(var4 stable)" 0 94)
  ("(var4 up)" 94 96)
  ("(var4 stable)" 96 99)
  ("(var4 up)" 99 137)
  ("(var4 stable)" 137 237)
  ("(var4 up)" 237 243)
  ("(var4 down)" 243 347)
  ("(var4 stable)" 347 386)
  ("(var1 stable)" 0 94)
  ("(var1 up)" 94 131)
  ("(var1 stable)" 131 386)
  ("(var2 stable)" 0 117)
  ("(var2 up)" 117 119)
  ("(var2 down)" 119 124)
  ("(var2 up)" 124 230)
  ("(var2 down)" 230 232)
  ("(var2 up)" 232 250)
  ("(var2 stable)" 250 386)
 )
)
(37
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 97)
  ("(var3 stable)" 97 173)
  ("(var3 up)" 173 176)
  ("(var3 down)" 176 185)
  ("(var3 stable)" 185 187)
  ("(var3 up)" 187 190)
  ("(var3 stable)" 190 314)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 114)
  ("(var4 stable)" 114 185)
  ("(var4 down)" 185 295)
  ("(var4 stable)" 295 314)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 98)
  ("(var1 stable)" 98 314)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 205)
  ("(var2 stable)" 205 314)
 )
)
(38
 (
  ("(var3 stable)" 0 77)
  ("(var3 down)" 77 79)
  ("(var3 up)" 79 108)
  ("(var3 stable)" 108 182)
  ("(var3 up)" 182 186)
  ("(var3 down)" 186 195)
  ("(var3 up)" 195 200)
  ("(var3 stable)" 200 328)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 105)
  ("(var4 stable)" 105 195)
  ("(var4 down)" 195 285)
  ("(var4 stable)" 285 328)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 105)
  ("(var1 stable)" 105 328)
  ("(var2 stable)" 0 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 187)
  ("(var2 down)" 187 189)
  ("(var2 up)" 189 217)
  ("(var2 stable)" 217 328)
 )
)
(39
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 117)
  ("(var3 stable)" 117 203)
  ("(var3 up)" 203 212)
  ("(var3 down)" 212 222)
  ("(var3 up)" 222 226)
  ("(var3 stable)" 226 378)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 89)
  ("(var4 stable)" 89 92)
  ("(var4 up)" 92 96)
  ("(var4 stable)" 96 98)
  ("(var4 up)" 98 122)
  ("(var4 stable)" 122 224)
  ("(var4 up)" 224 226)
  ("(var4 down)" 226 262)
  ("(var4 up)" 262 264)
  ("(var4 down)" 264 321)
  ("(var4 stable)" 321 378)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 115)
  ("(var1 stable)" 115 378)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 106)
  ("(var2 down)" 106 111)
  ("(var2 up)" 111 206)
  ("(var2 down)" 206 208)
  ("(var2 up)" 208 211)
  ("(var2 stable)" 211 214)
  ("(var2 up)" 214 259)
  ("(var2 stable)" 259 378)
 )
)
(40
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 92)
  ("(var3 stable)" 92 168)
  ("(var3 up)" 168 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 186)
  ("(var3 stable)" 186 317)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 102)
  ("(var4 stable)" 102 193)
  ("(var4 down)" 193 306)
  ("(var4 stable)" 306 317)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 86)
  ("(var1 stable)" 86 317)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 76)
  ("(var2 down)" 76 81)
  ("(var2 up)" 81 177)
  ("(var2 stable)" 177 179)
  ("(var2 up)" 179 183)
  ("(var2 stable)" 183 317)
 )
)
(41
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 88)
  ("(var3 stable)" 88 171)
  ("(var3 up)" 171 179)
  ("(var3 down)" 179 188)
  ("(var3 up)" 188 193)
  ("(var3 stable)" 193 334)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 99)
  ("(var4 stable)" 99 192)
  ("(var4 down)" 192 194)
  ("(var4 up)" 194 196)
  ("(var4 down)" 196 198)
  ("(var4 stable)" 198 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 297)
  ("(var4 stable)" 297 334)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 87)
  ("(var1 stable)" 87 334)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 stable)" 79 125)
  ("(var2 up)" 125 198)
  ("(var2 down)" 198 200)
  ("(var2 stable)" 200 334)
 )
)
(42
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 83)
  ("(var3 stable)" 83 152)
  ("(var3 up)" 152 158)
  ("(var3 down)" 158 167)
  ("(var3 up)" 167 172)
  ("(var3 stable)" 172 296)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 86)
  ("(var4 stable)" 86 167)
  ("(var4 down)" 167 275)
  ("(var4 stable)" 275 296)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 74)
  ("(var1 stable)" 74 296)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 175)
  ("(var2 stable)" 175 296)
 )
)
(43
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 63)
  ("(var3 up)" 63 93)
  ("(var3 stable)" 93 181)
  ("(var3 up)" 181 186)
  ("(var3 stable)" 186 188)
  ("(var3 down)" 188 197)
  ("(var3 up)" 197 206)
  ("(var3 stable)" 206 348)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 103)
  ("(var4 stable)" 103 203)
  ("(var4 down)" 203 320)
  ("(var4 stable)" 320 348)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 88)
  ("(var1 stable)" 88 348)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 209)
  ("(var2 down)" 209 211)
  ("(var2 up)" 211 213)
  ("(var2 stable)" 213 348)
 )
)
(44
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 90)
  ("(var3 stable)" 90 174)
  ("(var3 up)" 174 177)
  ("(var3 down)" 177 188)
  ("(var3 up)" 188 193)
  ("(var3 stable)" 193 325)
  ("(var3 up)" 325 327)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 95)
  ("(var4 stable)" 95 199)
  ("(var4 down)" 199 311)
  ("(var4 stable)" 311 327)
  ("(var1 stable)" 0 68)
  ("(var1 down)" 68 70)
  ("(var1 up)" 70 91)
  ("(var1 stable)" 91 327)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 210)
  ("(var2 stable)" 210 327)
 )
)
(45
 (
  ("(var3 stable)" 0 85)
  ("(var3 up)" 85 87)
  ("(var3 down)" 87 89)
  ("(var3 up)" 89 123)
  ("(var3 stable)" 123 209)
  ("(var3 up)" 209 213)
  ("(var3 down)" 213 223)
  ("(var3 up)" 223 229)
  ("(var3 stable)" 229 367)
  ("(var4 stable)" 0 93)
  ("(var4 up)" 93 126)
  ("(var4 stable)" 126 248)
  ("(var4 down)" 248 251)
  ("(var4 up)" 251 253)
  ("(var4 down)" 253 323)
  ("(var4 stable)" 323 367)
  ("(var1 stable)" 0 92)
  ("(var1 down)" 92 94)
  ("(var1 up)" 94 120)
  ("(var1 stable)" 120 367)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 109)
  ("(var2 down)" 109 114)
  ("(var2 up)" 114 246)
  ("(var2 stable)" 246 367)
 )
)
(46
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 98)
  ("(var3 stable)" 98 180)
  ("(var3 up)" 180 184)
  ("(var3 down)" 184 194)
  ("(var3 up)" 194 199)
  ("(var3 stable)" 199 337)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 103)
  ("(var4 stable)" 103 192)
  ("(var4 down)" 192 290)
  ("(var4 stable)" 290 337)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 71)
  ("(var1 stable)" 71 73)
  ("(var1 up)" 73 99)
  ("(var1 stable)" 99 337)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 stable)" 90 133)
  ("(var2 up)" 133 188)
  ("(var2 down)" 188 190)
  ("(var2 up)" 190 226)
  ("(var2 stable)" 226 337)
 )
)
(47
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 124)
  ("(var3 stable)" 124 206)
  ("(var3 up)" 206 210)
  ("(var3 down)" 210 221)
  ("(var3 up)" 221 227)
  ("(var3 stable)" 227 377)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 122)
  ("(var4 stable)" 122 128)
  ("(var4 up)" 128 130)
  ("(var4 stable)" 130 233)
  ("(var4 down)" 233 333)
  ("(var4 stable)" 333 377)
  ("(var1 stable)" 0 91)
  ("(var1 down)" 91 93)
  ("(var1 up)" 93 117)
  ("(var1 down)" 117 119)
  ("(var1 stable)" 119 377)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 106)
  ("(var2 down)" 106 111)
  ("(var2 up)" 111 237)
  ("(var2 down)" 237 239)
  ("(var2 up)" 239 249)
  ("(var2 stable)" 249 377)
 )
)
(48
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 79)
  ("(var3 stable)" 79 156)
  ("(var3 up)" 156 160)
  ("(var3 down)" 160 170)
  ("(var3 up)" 170 177)
  ("(var3 stable)" 177 307)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 43)
  ("(var4 stable)" 43 45)
  ("(var4 up)" 45 73)
  ("(var4 stable)" 73 75)
  ("(var4 up)" 75 78)
  ("(var4 stable)" 78 169)
  ("(var4 down)" 169 277)
  ("(var4 stable)" 277 307)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 71)
  ("(var1 down)" 71 73)
  ("(var1 stable)" 73 307)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 68)
  ("(var2 stable)" 68 107)
  ("(var2 up)" 107 205)
  ("(var2 stable)" 205 307)
 )
)
(49
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 66)
  ("(var3 down)" 66 68)
  ("(var3 up)" 68 70)
  ("(var3 stable)" 70 145)
  ("(var3 up)" 145 149)
  ("(var3 stable)" 149 151)
  ("(var3 down)" 151 160)
  ("(var3 up)" 160 164)
  ("(var3 stable)" 164 297)
  ("(var4 stable)" 0 30)
  ("(var4 up)" 30 73)
  ("(var4 stable)" 73 158)
  ("(var4 up)" 158 160)
  ("(var4 down)" 160 262)
  ("(var4 stable)" 262 297)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 63)
  ("(var1 stable)" 63 297)
  ("(var2 stable)" 0 49)
  ("(var2 up)" 49 53)
  ("(var2 down)" 53 57)
  ("(var2 up)" 57 173)
  ("(var2 down)" 173 175)
  ("(var2 stable)" 175 297)
 )
)
(50
 (
  ("(var3 stable)" 0 23)
  ("(var3 up)" 23 65)
  ("(var3 down)" 65 67)
  ("(var3 up)" 67 71)
  ("(var3 stable)" 71 155)
  ("(var3 up)" 155 160)
  ("(var3 down)" 160 170)
  ("(var3 stable)" 170 172)
  ("(var3 up)" 172 177)
  ("(var3 stable)" 177 315)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 80)
  ("(var4 stable)" 80 181)
  ("(var4 up)" 181 183)
  ("(var4 down)" 183 266)
  ("(var4 stable)" 266 315)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 51)
  ("(var1 down)" 51 53)
  ("(var1 up)" 53 66)
  ("(var1 stable)" 66 315)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 55)
  ("(var2 down)" 55 59)
  ("(var2 stable)" 59 103)
  ("(var2 up)" 103 182)
  ("(var2 down)" 182 184)
  ("(var2 up)" 184 189)
  ("(var2 stable)" 189 315)
 )
)
(51
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 86)
  ("(var3 stable)" 86 164)
  ("(var3 up)" 164 170)
  ("(var3 down)" 170 180)
  ("(var3 up)" 180 184)
  ("(var3 stable)" 184 320)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 84)
  ("(var4 stable)" 84 172)
  ("(var4 down)" 172 275)
  ("(var4 stable)" 275 320)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 53)
  ("(var1 down)" 53 55)
  ("(var1 up)" 55 82)
  ("(var1 stable)" 82 320)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 70)
  ("(var2 down)" 70 75)
  ("(var2 stable)" 75 119)
  ("(var2 up)" 119 208)
  ("(var2 stable)" 208 320)
 )
)
(52
 (
  ("(var3 stable)" 0 96)
  ("(var3 up)" 96 98)
  ("(var3 stable)" 98 101)
  ("(var3 up)" 101 134)
  ("(var3 stable)" 134 137)
  ("(var3 up)" 137 139)
  ("(var3 stable)" 139 219)
  ("(var3 up)" 219 224)
  ("(var3 down)" 224 233)
  ("(var3 up)" 233 240)
  ("(var3 stable)" 240 376)
  ("(var4 stable)" 0 95)
  ("(var4 up)" 95 140)
  ("(var4 stable)" 140 257)
  ("(var4 down)" 257 264)
  ("(var4 stable)" 264 266)
  ("(var4 down)" 266 326)
  ("(var4 stable)" 326 376)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 94)
  ("(var1 down)" 94 96)
  ("(var1 up)" 96 98)
  ("(var1 down)" 98 100)
  ("(var1 up)" 100 126)
  ("(var1 stable)" 126 128)
  ("(var1 up)" 128 134)
  ("(var1 stable)" 134 376)
  ("(var2 stable)" 0 113)
  ("(var2 up)" 113 120)
  ("(var2 down)" 120 128)
  ("(var2 up)" 128 259)
  ("(var2 stable)" 259 376)
 )
)
(53
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 63)
  ("(var3 down)" 63 66)
  ("(var3 up)" 66 94)
  ("(var3 stable)" 94 97)
  ("(var3 up)" 97 99)
  ("(var3 down)" 99 101)
  ("(var3 up)" 101 103)
  ("(var3 stable)" 103 177)
  ("(var3 up)" 177 182)
  ("(var3 down)" 182 191)
  ("(var3 stable)" 191 193)
  ("(var3 up)" 193 195)
  ("(var3 stable)" 195 333)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 93)
  ("(var4 stable)" 93 95)
  ("(var4 up)" 95 98)
  ("(var4 stable)" 98 192)
  ("(var4 down)" 192 279)
  ("(var4 stable)" 279 333)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 91)
  ("(var1 stable)" 91 333)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 217)
  ("(var2 stable)" 217 331)
  ("(var2 down)" 331 333)
 )
)
(54
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 72)
  ("(var3 stable)" 72 159)
  ("(var3 up)" 159 163)
  ("(var3 down)" 163 173)
  ("(var3 up)" 173 179)
  ("(var3 stable)" 179 317)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 73)
  ("(var4 down)" 73 75)
  ("(var4 stable)" 75 199)
  ("(var4 down)" 199 201)
  ("(var4 up)" 201 203)
  ("(var4 down)" 203 272)
  ("(var4 stable)" 272 315)
  ("(var4 down)" 315 317)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 73)
  ("(var1 stable)" 73 317)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 66)
  ("(var2 stable)" 66 97)
  ("(var2 up)" 97 171)
  ("(var2 stable)" 171 317)
 )
)
(55
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 101)
  ("(var3 stable)" 101 187)
  ("(var3 up)" 187 193)
  ("(var3 down)" 193 204)
  ("(var3 stable)" 204 349)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 106)
  ("(var4 stable)" 106 194)
  ("(var4 down)" 194 196)
  ("(var4 up)" 196 198)
  ("(var4 stable)" 198 232)
  ("(var4 down)" 232 304)
  ("(var4 up)" 304 306)
  ("(var4 down)" 306 308)
  ("(var4 stable)" 308 349)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 100)
  ("(var1 down)" 100 103)
  ("(var1 stable)" 103 349)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 up)" 92 225)
  ("(var2 stable)" 225 349)
 )
)
(56
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 86)
  ("(var3 stable)" 86 164)
  ("(var3 up)" 164 167)
  ("(var3 down)" 167 177)
  ("(var3 up)" 177 181)
  ("(var3 stable)" 181 302)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 85)
  ("(var4 stable)" 85 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 166)
  ("(var4 down)" 166 269)
  ("(var4 stable)" 269 302)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 84)
  ("(var1 stable)" 84 302)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 77)
  ("(var2 up)" 77 247)
  ("(var2 stable)" 247 302)
 )
)
(57
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 86)
  ("(var3 stable)" 86 89)
  ("(var3 up)" 89 119)
  ("(var3 stable)" 119 190)
  ("(var3 up)" 190 196)
  ("(var3 down)" 196 204)
  ("(var3 up)" 204 209)
  ("(var3 stable)" 209 343)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 115)
  ("(var4 stable)" 115 211)
  ("(var4 down)" 211 297)
  ("(var4 stable)" 297 343)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 91)
  ("(var1 stable)" 91 93)
  ("(var1 up)" 93 113)
  ("(var1 stable)" 113 343)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 103)
  ("(var2 down)" 103 108)
  ("(var2 stable)" 108 142)
  ("(var2 up)" 142 230)
  ("(var2 stable)" 230 233)
  ("(var2 up)" 233 236)
  ("(var2 stable)" 236 343)
 )
)
(58
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 71)
  ("(var3 stable)" 71 154)
  ("(var3 up)" 154 160)
  ("(var3 down)" 160 170)
  ("(var3 up)" 170 175)
  ("(var3 stable)" 175 316)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 80)
  ("(var4 stable)" 80 197)
  ("(var4 up)" 197 199)
  ("(var4 down)" 199 202)
  ("(var4 up)" 202 205)
  ("(var4 down)" 205 266)
  ("(var4 stable)" 266 316)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 65)
  ("(var1 down)" 65 67)
  ("(var1 up)" 67 71)
  ("(var1 stable)" 71 316)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 216)
  ("(var2 stable)" 216 316)
 )
)
(59
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 78)
  ("(var3 stable)" 78 157)
  ("(var3 up)" 157 161)
  ("(var3 down)" 161 174)
  ("(var3 up)" 174 179)
  ("(var3 stable)" 179 323)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 46)
  ("(var4 stable)" 46 49)
  ("(var4 up)" 49 73)
  ("(var4 stable)" 73 198)
  ("(var4 down)" 198 272)
  ("(var4 stable)" 272 323)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 82)
  ("(var1 stable)" 82 323)
  ("(var2 stable)" 0 58)
  ("(var2 up)" 58 62)
  ("(var2 down)" 62 66)
  ("(var2 stable)" 66 108)
  ("(var2 up)" 108 204)
  ("(var2 stable)" 204 323)
 )
)
(60
 (
  ("(var3 stable)" 0 102)
  ("(var3 up)" 102 136)
  ("(var3 stable)" 136 222)
  ("(var3 up)" 222 227)
  ("(var3 down)" 227 238)
  ("(var3 up)" 238 241)
  ("(var3 stable)" 241 381)
  ("(var4 stable)" 0 96)
  ("(var4 up)" 96 100)
  ("(var4 down)" 100 102)
  ("(var4 up)" 102 133)
  ("(var4 stable)" 133 135)
  ("(var4 up)" 135 140)
  ("(var4 stable)" 140 245)
  ("(var4 down)" 245 342)
  ("(var4 stable)" 342 381)
  ("(var1 stable)" 0 101)
  ("(var1 up)" 101 128)
  ("(var1 stable)" 128 381)
  ("(var2 stable)" 0 116)
  ("(var2 up)" 116 118)
  ("(var2 down)" 118 123)
  ("(var2 stable)" 123 171)
  ("(var2 up)" 171 247)
  ("(var2 down)" 247 250)
  ("(var2 up)" 250 253)
  ("(var2 stable)" 253 381)
 )
)
(61
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 93)
  ("(var3 stable)" 93 178)
  ("(var3 up)" 178 184)
  ("(var3 down)" 184 194)
  ("(var3 up)" 194 200)
  ("(var3 stable)" 200 341)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 97)
  ("(var4 down)" 97 99)
  ("(var4 stable)" 99 223)
  ("(var4 down)" 223 307)
  ("(var4 stable)" 307 341)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 74)
  ("(var1 stable)" 74 76)
  ("(var1 up)" 76 95)
  ("(var1 stable)" 95 341)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 136)
  ("(var2 down)" 136 138)
  ("(var2 up)" 138 216)
  ("(var2 down)" 216 218)
  ("(var2 stable)" 218 341)
 )
)
(62
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 120)
  ("(var3 stable)" 120 200)
  ("(var3 up)" 200 205)
  ("(var3 down)" 205 215)
  ("(var3 up)" 215 219)
  ("(var3 stable)" 219 359)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 115)
  ("(var4 stable)" 115 246)
  ("(var4 down)" 246 332)
  ("(var4 up)" 332 334)
  ("(var4 down)" 334 336)
  ("(var4 stable)" 336 359)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 114)
  ("(var1 stable)" 114 359)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 105)
  ("(var2 down)" 105 109)
  ("(var2 up)" 109 215)
  ("(var2 stable)" 215 217)
  ("(var2 up)" 217 219)
  ("(var2 stable)" 219 359)
 )
)
(63
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 68)
  ("(var3 stable)" 68 156)
  ("(var3 up)" 156 162)
  ("(var3 down)" 162 172)
  ("(var3 up)" 172 179)
  ("(var3 stable)" 179 321)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 58)
  ("(var4 stable)" 58 60)
  ("(var4 up)" 60 70)
  ("(var4 stable)" 70 184)
  ("(var4 down)" 184 186)
  ("(var4 up)" 186 188)
  ("(var4 down)" 188 203)
  ("(var4 up)" 203 205)
  ("(var4 down)" 205 278)
  ("(var4 stable)" 278 321)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 66)
  ("(var1 down)" 66 68)
  ("(var1 up)" 68 70)
  ("(var1 stable)" 70 321)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 50)
  ("(var2 up)" 50 54)
  ("(var2 down)" 54 62)
  ("(var2 stable)" 62 65)
  ("(var2 up)" 65 186)
  ("(var2 down)" 186 188)
  ("(var2 up)" 188 190)
  ("(var2 stable)" 190 321)
 )
)
(64
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 113)
  ("(var3 stable)" 113 115)
  ("(var3 up)" 115 123)
  ("(var3 stable)" 123 197)
  ("(var3 up)" 197 202)
  ("(var3 down)" 202 212)
  ("(var3 up)" 212 217)
  ("(var3 stable)" 217 349)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 125)
  ("(var4 down)" 125 127)
  ("(var4 stable)" 127 220)
  ("(var4 down)" 220 302)
  ("(var4 up)" 302 304)
  ("(var4 down)" 304 312)
  ("(var4 stable)" 312 349)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 89)
  ("(var1 down)" 89 91)
  ("(var1 up)" 91 112)
  ("(var1 stable)" 112 349)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 stable)" 109 147)
  ("(var2 up)" 147 149)
  ("(var2 stable)" 149 152)
  ("(var2 up)" 152 240)
  ("(var2 stable)" 240 346)
  ("(var2 up)" 346 349)
 )
)
(65
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 114)
  ("(var3 stable)" 114 199)
  ("(var3 up)" 199 203)
  ("(var3 down)" 203 215)
  ("(var3 up)" 215 220)
  ("(var3 stable)" 220 351)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 115)
  ("(var4 down)" 115 117)
  ("(var4 up)" 117 119)
  ("(var4 stable)" 119 213)
  ("(var4 down)" 213 308)
  ("(var4 stable)" 308 351)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 111)
  ("(var1 stable)" 111 351)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 231)
  ("(var2 stable)" 231 351)
 )
)
(66
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 69)
  ("(var3 stable)" 69 139)
  ("(var3 up)" 139 142)
  ("(var3 down)" 142 151)
  ("(var3 stable)" 151 153)
  ("(var3 up)" 153 156)
  ("(var3 stable)" 156 281)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 65)
  ("(var4 stable)" 65 155)
  ("(var4 up)" 155 157)
  ("(var4 down)" 157 241)
  ("(var4 stable)" 241 246)
  ("(var4 down)" 246 248)
  ("(var4 stable)" 248 281)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 59)
  ("(var1 stable)" 59 281)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 57)
  ("(var2 up)" 57 143)
  ("(var2 down)" 143 145)
  ("(var2 up)" 145 171)
  ("(var2 stable)" 171 281)
 )
)
(67
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 75)
  ("(var3 stable)" 75 142)
  ("(var3 up)" 142 148)
  ("(var3 down)" 148 157)
  ("(var3 up)" 157 162)
  ("(var3 stable)" 162 289)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 47)
  ("(var4 stable)" 47 49)
  ("(var4 up)" 49 69)
  ("(var4 stable)" 69 71)
  ("(var4 up)" 71 74)
  ("(var4 stable)" 74 145)
  ("(var4 up)" 145 148)
  ("(var4 down)" 148 189)
  ("(var4 stable)" 189 191)
  ("(var4 down)" 191 257)
  ("(var4 stable)" 257 289)
  ("(var1 stable)" 0 47)
  ("(var1 down)" 47 49)
  ("(var1 up)" 49 67)
  ("(var1 down)" 67 69)
  ("(var1 stable)" 69 289)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 183)
  ("(var2 down)" 183 185)
  ("(var2 up)" 185 188)
  ("(var2 stable)" 188 289)
 )
)
(68
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 72)
  ("(var3 stable)" 72 147)
  ("(var3 up)" 147 152)
  ("(var3 down)" 152 161)
  ("(var3 up)" 161 167)
  ("(var3 stable)" 167 295)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 74)
  ("(var4 stable)" 74 184)
  ("(var4 up)" 184 186)
  ("(var4 down)" 186 188)
  ("(var4 stable)" 188 190)
  ("(var4 down)" 190 275)
  ("(var4 stable)" 275 295)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 42)
  ("(var1 down)" 42 44)
  ("(var1 up)" 44 67)
  ("(var1 stable)" 67 293)
  ("(var1 down)" 293 295)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 stable)" 62 103)
  ("(var2 up)" 103 161)
  ("(var2 stable)" 161 198)
  ("(var2 down)" 198 201)
  ("(var2 up)" 201 203)
  ("(var2 stable)" 203 295)
 )
)
(69
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 80)
  ("(var3 stable)" 80 82)
  ("(var3 up)" 82 104)
  ("(var3 stable)" 104 173)
  ("(var3 up)" 173 177)
  ("(var3 down)" 177 185)
  ("(var3 up)" 185 189)
  ("(var3 stable)" 189 309)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 106)
  ("(var4 stable)" 106 183)
  ("(var4 down)" 183 307)
  ("(var4 stable)" 307 309)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 98)
  ("(var1 stable)" 98 309)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 92)
  ("(var2 down)" 92 97)
  ("(var2 up)" 97 223)
  ("(var2 stable)" 223 309)
 )
)
(70
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 51)
  ("(var3 up)" 51 53)
  ("(var3 stable)" 53 55)
  ("(var3 up)" 55 85)
  ("(var3 stable)" 85 164)
  ("(var3 up)" 164 172)
  ("(var3 down)" 172 184)
  ("(var3 up)" 184 190)
  ("(var3 stable)" 190 331)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 91)
  ("(var4 stable)" 91 192)
  ("(var4 down)" 192 229)
  ("(var4 stable)" 229 231)
  ("(var4 down)" 231 292)
  ("(var4 stable)" 292 331)
  ("(var1 stable)" 0 51)
  ("(var1 down)" 51 57)
  ("(var1 up)" 57 79)
  ("(var1 stable)" 79 331)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 70)
  ("(var2 down)" 70 75)
  ("(var2 up)" 75 169)
  ("(var2 down)" 169 171)
  ("(var2 up)" 171 215)
  ("(var2 stable)" 215 331)
 )
)
(71
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 83)
  ("(var3 stable)" 83 161)
  ("(var3 up)" 161 166)
  ("(var3 down)" 166 176)
  ("(var3 up)" 176 181)
  ("(var3 stable)" 181 319)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 47)
  ("(var4 down)" 47 49)
  ("(var4 up)" 49 83)
  ("(var4 stable)" 83 178)
  ("(var4 down)" 178 181)
  ("(var4 up)" 181 184)
  ("(var4 down)" 184 189)
  ("(var4 up)" 189 191)
  ("(var4 down)" 191 275)
  ("(var4 stable)" 275 319)
  ("(var1 up)" 0 2)
  ("(var1 stable)" 2 46)
  ("(var1 up)" 46 78)
  ("(var1 stable)" 78 319)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 stable)" 69 107)
  ("(var2 up)" 107 210)
  ("(var2 down)" 210 212)
  ("(var2 up)" 212 215)
  ("(var2 stable)" 215 319)
 )
)
(72
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 56)
  ("(var3 down)" 56 58)
  ("(var3 up)" 58 61)
  ("(var3 down)" 61 63)
  ("(var3 up)" 63 98)
  ("(var3 stable)" 98 181)
  ("(var3 up)" 181 185)
  ("(var3 down)" 185 195)
  ("(var3 up)" 195 200)
  ("(var3 stable)" 200 343)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 89)
  ("(var4 stable)" 89 226)
  ("(var4 down)" 226 296)
  ("(var4 stable)" 296 343)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 84)
  ("(var1 stable)" 84 343)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 75)
  ("(var2 down)" 75 79)
  ("(var2 stable)" 79 123)
  ("(var2 up)" 123 193)
  ("(var2 stable)" 193 195)
  ("(var2 up)" 195 197)
  ("(var2 stable)" 197 343)
 )
)
(73
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 68)
  ("(var3 stable)" 68 156)
  ("(var3 up)" 156 160)
  ("(var3 down)" 160 172)
  ("(var3 up)" 172 179)
  ("(var3 stable)" 179 326)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 69)
  ("(var4 stable)" 69 186)
  ("(var4 down)" 186 262)
  ("(var4 up)" 262 264)
  ("(var4 down)" 264 286)
  ("(var4 stable)" 286 326)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 62)
  ("(var1 stable)" 62 326)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 up)" 58 204)
  ("(var2 stable)" 204 326)
 )
)
(74
 (
  ("(var3 stable)" 0 71)
  ("(var3 down)" 71 73)
  ("(var3 stable)" 73 76)
  ("(var3 up)" 76 106)
  ("(var3 stable)" 106 195)
  ("(var3 up)" 195 200)
  ("(var3 down)" 200 212)
  ("(var3 up)" 212 216)
  ("(var3 stable)" 216 358)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 107)
  ("(var4 stable)" 107 236)
  ("(var4 down)" 236 328)
  ("(var4 stable)" 328 358)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 102)
  ("(var1 stable)" 102 358)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 237)
  ("(var2 down)" 237 239)
  ("(var2 stable)" 239 358)
 )
)
(75
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 113)
  ("(var3 stable)" 113 117)
  ("(var3 up)" 117 119)
  ("(var3 stable)" 119 191)
  ("(var3 up)" 191 196)
  ("(var3 down)" 196 206)
  ("(var3 up)" 206 210)
  ("(var3 stable)" 210 342)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 91)
  ("(var4 stable)" 91 93)
  ("(var4 up)" 93 124)
  ("(var4 stable)" 124 205)
  ("(var4 down)" 205 207)
  ("(var4 up)" 207 209)
  ("(var4 down)" 209 292)
  ("(var4 stable)" 292 294)
  ("(var4 down)" 294 306)
  ("(var4 stable)" 306 342)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 114)
  ("(var1 stable)" 114 342)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 107)
  ("(var2 up)" 107 236)
  ("(var2 stable)" 236 342)
 )
)
(76
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 108)
  ("(var3 stable)" 108 182)
  ("(var3 up)" 182 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 203)
  ("(var3 stable)" 203 337)
  ("(var4 stable)" 0 72)
  ("(var4 down)" 72 74)
  ("(var4 up)" 74 101)
  ("(var4 down)" 101 103)
  ("(var4 stable)" 103 211)
  ("(var4 down)" 211 315)
  ("(var4 up)" 315 317)
  ("(var4 stable)" 317 337)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 97)
  ("(var1 stable)" 97 337)
  ("(var2 stable)" 0 86)
  ("(var2 up)" 86 88)
  ("(var2 down)" 88 93)
  ("(var2 up)" 93 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 214)
  ("(var2 stable)" 214 337)
 )
)
(77
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 61)
  ("(var3 stable)" 61 132)
  ("(var3 up)" 132 135)
  ("(var3 down)" 135 145)
  ("(var3 up)" 145 148)
  ("(var3 stable)" 148 274)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 67)
  ("(var4 stable)" 67 142)
  ("(var4 down)" 142 235)
  ("(var4 up)" 235 237)
  ("(var4 down)" 237 239)
  ("(var4 stable)" 239 274)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 56)
  ("(var1 stable)" 56 274)
  ("(var2 stable)" 0 43)
  ("(var2 up)" 43 45)
  ("(var2 down)" 45 50)
  ("(var2 stable)" 50 87)
  ("(var2 up)" 87 160)
  ("(var2 stable)" 160 274)
 )
)
(78
 (
  ("(var3 stable)" 0 98)
  ("(var3 up)" 98 135)
  ("(var3 stable)" 135 217)
  ("(var3 up)" 217 222)
  ("(var3 stable)" 222 224)
  ("(var3 down)" 224 233)
  ("(var3 stable)" 233 235)
  ("(var3 up)" 235 237)
  ("(var3 stable)" 237 376)
  ("(var4 stable)" 0 98)
  ("(var4 up)" 98 132)
  ("(var4 stable)" 132 249)
  ("(var4 down)" 249 320)
  ("(var4 stable)" 320 322)
  ("(var4 down)" 322 332)
  ("(var4 stable)" 332 376)
  ("(var1 stable)" 0 94)
  ("(var1 up)" 94 129)
  ("(var1 stable)" 129 376)
  ("(var2 stable)" 0 114)
  ("(var2 up)" 114 118)
  ("(var2 down)" 118 122)
  ("(var2 up)" 122 267)
  ("(var2 stable)" 267 376)
 )
)
(79
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 114)
  ("(var3 stable)" 114 116)
  ("(var3 up)" 116 118)
  ("(var3 stable)" 118 191)
  ("(var3 up)" 191 195)
  ("(var3 down)" 195 202)
  ("(var3 stable)" 202 204)
  ("(var3 up)" 204 209)
  ("(var3 stable)" 209 328)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 119)
  ("(var4 down)" 119 121)
  ("(var4 stable)" 121 203)
  ("(var4 down)" 203 285)
  ("(var4 stable)" 285 290)
  ("(var4 down)" 290 293)
  ("(var4 stable)" 293 328)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 110)
  ("(var1 stable)" 110 328)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 101)
  ("(var2 down)" 101 106)
  ("(var2 up)" 106 226)
  ("(var2 stable)" 226 328)
 )
)
(80
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 86)
  ("(var3 stable)" 86 166)
  ("(var3 up)" 166 173)
  ("(var3 down)" 173 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 330)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 90)
  ("(var4 stable)" 90 184)
  ("(var4 down)" 184 285)
  ("(var4 stable)" 285 321)
  ("(var4 up)" 321 323)
  ("(var4 stable)" 323 330)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 81)
  ("(var1 stable)" 81 330)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 stable)" 76 120)
  ("(var2 up)" 120 218)
  ("(var2 stable)" 218 330)
 )
)
(81
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 93)
  ("(var3 stable)" 93 172)
  ("(var3 up)" 172 175)
  ("(var3 down)" 175 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 323)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 58)
  ("(var4 down)" 58 60)
  ("(var4 up)" 60 94)
  ("(var4 stable)" 94 186)
  ("(var4 down)" 186 277)
  ("(var4 stable)" 277 323)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 92)
  ("(var1 stable)" 92 323)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 174)
  ("(var2 stable)" 174 176)
  ("(var2 up)" 176 204)
  ("(var2 stable)" 204 323)
 )
)
(82
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 103)
  ("(var3 stable)" 103 178)
  ("(var3 up)" 178 183)
  ("(var3 down)" 183 192)
  ("(var3 up)" 192 196)
  ("(var3 stable)" 196 321)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 108)
  ("(var4 stable)" 108 191)
  ("(var4 down)" 191 281)
  ("(var4 stable)" 281 318)
  ("(var4 up)" 318 321)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 97)
  ("(var1 stable)" 97 321)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 94)
  ("(var2 up)" 94 207)
  ("(var2 down)" 207 209)
  ("(var2 stable)" 209 321)
 )
)
(83
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 68)
  ("(var3 stable)" 68 148)
  ("(var3 up)" 148 152)
  ("(var3 down)" 152 162)
  ("(var3 up)" 162 169)
  ("(var3 stable)" 169 299)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 70)
  ("(var4 stable)" 70 177)
  ("(var4 down)" 177 243)
  ("(var4 up)" 243 245)
  ("(var4 down)" 245 247)
  ("(var4 up)" 247 249)
  ("(var4 down)" 249 252)
  ("(var4 stable)" 252 299)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 65)
  ("(var1 stable)" 65 299)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 60)
  ("(var2 stable)" 60 102)
  ("(var2 up)" 102 191)
  ("(var2 stable)" 191 299)
 )
)
(84
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 117)
  ("(var3 stable)" 117 193)
  ("(var3 up)" 193 197)
  ("(var3 down)" 197 209)
  ("(var3 up)" 209 215)
  ("(var3 stable)" 215 349)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 119)
  ("(var4 stable)" 119 216)
  ("(var4 up)" 216 218)
  ("(var4 down)" 218 323)
  ("(var4 stable)" 323 349)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 114)
  ("(var1 stable)" 114 349)
  ("(var2 stable)" 0 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 104)
  ("(var2 up)" 104 203)
  ("(var2 down)" 203 205)
  ("(var2 up)" 205 244)
  ("(var2 stable)" 244 349)
 )
)
(85
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 118)
  ("(var3 stable)" 118 206)
  ("(var3 up)" 206 210)
  ("(var3 down)" 210 222)
  ("(var3 stable)" 222 224)
  ("(var3 up)" 224 231)
  ("(var3 stable)" 231 378)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 123)
  ("(var4 stable)" 123 244)
  ("(var4 down)" 244 247)
  ("(var4 stable)" 247 249)
  ("(var4 down)" 249 336)
  ("(var4 stable)" 336 378)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 114)
  ("(var1 stable)" 114 378)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 106)
  ("(var2 down)" 106 110)
  ("(var2 stable)" 110 158)
  ("(var2 up)" 158 248)
  ("(var2 stable)" 248 378)
 )
)
(86
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 99)
  ("(var3 stable)" 99 175)
  ("(var3 up)" 175 179)
  ("(var3 down)" 179 189)
  ("(var3 up)" 189 194)
  ("(var3 stable)" 194 329)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 95)
  ("(var4 stable)" 95 196)
  ("(var4 down)" 196 300)
  ("(var4 stable)" 300 329)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 90)
  ("(var1 stable)" 90 329)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 86)
  ("(var2 stable)" 86 121)
  ("(var2 up)" 121 210)
  ("(var2 stable)" 210 329)
 )
)
(87
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 97)
  ("(var3 stable)" 97 166)
  ("(var3 up)" 166 171)
  ("(var3 down)" 171 178)
  ("(var3 up)" 178 185)
  ("(var3 stable)" 185 312)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 96)
  ("(var4 stable)" 96 98)
  ("(var4 up)" 98 100)
  ("(var4 stable)" 100 180)
  ("(var4 down)" 180 265)
  ("(var4 stable)" 265 267)
  ("(var4 down)" 267 271)
  ("(var4 stable)" 271 312)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 90)
  ("(var1 stable)" 90 312)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 84)
  ("(var2 down)" 84 87)
  ("(var2 up)" 87 243)
  ("(var2 stable)" 243 312)
 )
)
(88
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 86)
  ("(var3 stable)" 86 159)
  ("(var3 up)" 159 165)
  ("(var3 down)" 165 175)
  ("(var3 up)" 175 180)
  ("(var3 stable)" 180 315)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 80)
  ("(var4 stable)" 80 165)
  ("(var4 down)" 165 167)
  ("(var4 up)" 167 169)
  ("(var4 down)" 169 277)
  ("(var4 stable)" 277 315)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 75)
  ("(var1 stable)" 75 315)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 up)" 71 169)
  ("(var2 stable)" 169 171)
  ("(var2 up)" 171 197)
  ("(var2 stable)" 197 315)
 )
)
(89
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 92)
  ("(var3 stable)" 92 166)
  ("(var3 up)" 166 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 186)
  ("(var3 stable)" 186 320)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 90)
  ("(var4 stable)" 90 174)
  ("(var4 down)" 174 290)
  ("(var4 stable)" 290 320)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 84)
  ("(var1 stable)" 84 320)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 75)
  ("(var2 down)" 75 80)
  ("(var2 up)" 80 178)
  ("(var2 down)" 178 181)
  ("(var2 up)" 181 214)
  ("(var2 stable)" 214 320)
 )
)
(90
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 92)
  ("(var3 stable)" 92 169)
  ("(var3 up)" 169 174)
  ("(var3 down)" 174 183)
  ("(var3 stable)" 183 185)
  ("(var3 up)" 185 187)
  ("(var3 stable)" 187 324)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 91)
  ("(var4 stable)" 91 180)
  ("(var4 down)" 180 274)
  ("(var4 stable)" 274 324)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 85)
  ("(var1 stable)" 85 324)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 213)
  ("(var2 stable)" 213 324)
 )
)
(91
 (
  ("(var3 up)" 0 4)
  ("(var3 down)" 4 7)
  ("(var3 stable)" 7 52)
  ("(var3 up)" 52 79)
  ("(var3 stable)" 79 165)
  ("(var3 up)" 165 167)
  ("(var3 down)" 167 177)
  ("(var3 stable)" 177 179)
  ("(var3 up)" 179 184)
  ("(var3 stable)" 184 322)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 82)
  ("(var4 stable)" 82 204)
  ("(var4 down)" 204 274)
  ("(var4 stable)" 274 322)
  ("(var1 stable)" 0 54)
  ("(var1 up)" 54 77)
  ("(var1 stable)" 77 322)
  ("(var2 stable)" 0 65)
  ("(var2 up)" 65 69)
  ("(var2 down)" 69 72)
  ("(var2 up)" 72 222)
  ("(var2 stable)" 222 322)
 )
)
(92
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 72)
  ("(var3 stable)" 72 138)
  ("(var3 up)" 138 143)
  ("(var3 down)" 143 153)
  ("(var3 up)" 153 155)
  ("(var3 stable)" 155 282)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 65)
  ("(var4 stable)" 65 152)
  ("(var4 down)" 152 256)
  ("(var4 stable)" 256 282)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 62)
  ("(var1 stable)" 62 282)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 54)
  ("(var2 down)" 54 56)
  ("(var2 stable)" 56 94)
  ("(var2 up)" 94 171)
  ("(var2 stable)" 171 282)
 )
)
(93
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 86)
  ("(var3 down)" 86 88)
  ("(var3 up)" 88 91)
  ("(var3 stable)" 91 93)
  ("(var3 up)" 93 126)
  ("(var3 stable)" 126 200)
  ("(var3 up)" 200 205)
  ("(var3 down)" 205 217)
  ("(var3 up)" 217 220)
  ("(var3 stable)" 220 364)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 114)
  ("(var4 down)" 114 116)
  ("(var4 up)" 116 118)
  ("(var4 stable)" 118 224)
  ("(var4 down)" 224 338)
  ("(var4 stable)" 338 364)
  ("(var1 stable)" 0 86)
  ("(var1 down)" 86 88)
  ("(var1 up)" 88 117)
  ("(var1 stable)" 117 364)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 104)
  ("(var2 down)" 104 108)
  ("(var2 up)" 108 243)
  ("(var2 down)" 243 245)
  ("(var2 stable)" 245 364)
 )
)
(94
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 50)
  ("(var3 stable)" 50 52)
  ("(var3 up)" 52 78)
  ("(var3 stable)" 78 152)
  ("(var3 up)" 152 155)
  ("(var3 down)" 155 165)
  ("(var3 up)" 165 170)
  ("(var3 stable)" 170 294)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 77)
  ("(var4 stable)" 77 155)
  ("(var4 down)" 155 157)
  ("(var4 up)" 157 159)
  ("(var4 down)" 159 251)
  ("(var4 stable)" 251 294)
  ("(var1 stable)" 0 50)
  ("(var1 down)" 50 52)
  ("(var1 up)" 52 69)
  ("(var1 down)" 69 71)
  ("(var1 up)" 71 73)
  ("(var1 stable)" 73 294)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 67)
  ("(var2 up)" 67 190)
  ("(var2 stable)" 190 294)
 )
)
(95
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 78)
  ("(var3 up)" 78 115)
  ("(var3 stable)" 115 202)
  ("(var3 up)" 202 206)
  ("(var3 down)" 206 218)
  ("(var3 up)" 218 223)
  ("(var3 stable)" 223 367)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 137)
  ("(var4 stable)" 137 229)
  ("(var4 down)" 229 332)
  ("(var4 stable)" 332 367)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 112)
  ("(var1 stable)" 112 367)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 103)
  ("(var2 down)" 103 107)
  ("(var2 up)" 107 208)
  ("(var2 stable)" 208 210)
  ("(var2 up)" 210 250)
  ("(var2 stable)" 250 367)
 )
)
(96
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 96)
  ("(var3 down)" 96 98)
  ("(var3 up)" 98 100)
  ("(var3 stable)" 100 176)
  ("(var3 up)" 176 182)
  ("(var3 down)" 182 192)
  ("(var3 up)" 192 196)
  ("(var3 stable)" 196 331)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 97)
  ("(var4 stable)" 97 201)
  ("(var4 down)" 201 203)
  ("(var4 up)" 203 205)
  ("(var4 down)" 205 211)
  ("(var4 up)" 211 213)
  ("(var4 down)" 213 287)
  ("(var4 stable)" 287 331)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 89)
  ("(var1 stable)" 89 331)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 204)
  ("(var2 stable)" 204 331)
 )
)
(97
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 112)
  ("(var3 stable)" 112 186)
  ("(var3 up)" 186 188)
  ("(var3 down)" 188 197)
  ("(var3 up)" 197 199)
  ("(var3 stable)" 199 319)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 125)
  ("(var4 stable)" 125 201)
  ("(var4 down)" 201 211)
  ("(var4 up)" 211 213)
  ("(var4 down)" 213 215)
  ("(var4 stable)" 215 217)
  ("(var4 down)" 217 272)
  ("(var4 stable)" 272 275)
  ("(var4 down)" 275 279)
  ("(var4 stable)" 279 319)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 110)
  ("(var1 down)" 110 112)
  ("(var1 stable)" 112 319)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 103)
  ("(var2 up)" 103 261)
  ("(var2 stable)" 261 319)
 )
)
(98
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 92)
  ("(var3 stable)" 92 174)
  ("(var3 up)" 174 178)
  ("(var3 down)" 178 188)
  ("(var3 up)" 188 194)
  ("(var3 stable)" 194 323)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 97)
  ("(var4 stable)" 97 195)
  ("(var4 down)" 195 282)
  ("(var4 stable)" 282 323)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 92)
  ("(var1 stable)" 92 323)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 205)
  ("(var2 stable)" 205 323)
 )
)
(99
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 103)
  ("(var3 stable)" 103 188)
  ("(var3 up)" 188 193)
  ("(var3 down)" 193 203)
  ("(var3 up)" 203 205)
  ("(var3 stable)" 205 342)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 112)
  ("(var4 stable)" 112 199)
  ("(var4 down)" 199 296)
  ("(var4 stable)" 296 342)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 104)
  ("(var1 stable)" 104 342)
  ("(var2 stable)" 0 91)
  ("(var2 up)" 91 93)
  ("(var2 down)" 93 98)
  ("(var2 up)" 98 238)
  ("(var2 stable)" 238 342)
 )
)
(100
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 114)
  ("(var3 stable)" 114 200)
  ("(var3 up)" 200 205)
  ("(var3 down)" 205 216)
  ("(var3 up)" 216 220)
  ("(var3 stable)" 220 368)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 77)
  ("(var4 stable)" 77 79)
  ("(var4 up)" 79 121)
  ("(var4 stable)" 121 224)
  ("(var4 down)" 224 226)
  ("(var4 up)" 226 228)
  ("(var4 down)" 228 312)
  ("(var4 stable)" 312 324)
  ("(var4 down)" 324 326)
  ("(var4 stable)" 326 368)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 103)
  ("(var1 stable)" 103 368)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 stable)" 101 147)
  ("(var2 up)" 147 223)
  ("(var2 stable)" 223 228)
  ("(var2 up)" 228 230)
  ("(var2 down)" 230 232)
  ("(var2 up)" 232 234)
  ("(var2 stable)" 234 368)
 )
)
